Robinson's joint consistency theorem

Robinson's joint consistency theorem is an important theorem of mathematical logic. It is related to Craig interpolation and Beth definability.

The classical formulation of Robinson's joint consistency theorem is as follows:

Let $T_1$ and $T_2$ be first-order theories. If $T_1$ and $T_2$ are consistent and the intersection $T_1\cap T_2$ is complete (in the common language of $T_1$ and $T_2$ ), then the union $T_1\cup T_2$ is consistent. Note that a theory is complete if it decides every formula, i.e. either $T \vdash \varphi$ or $T \vdash \neg\varphi$ .

Since the completeness assumption is quite hard to fulfill, there is a variant of the theorem:

Let $T_1$ and $T_2$ be first-order theories. If $T_1$ and $T_2$ are consistent and if there is no formula $\varphi$ in the common language of $T_1$ and $T_2$ such that $T_1 \vdash \varphi$ and $T_2 \vdash \neg\varphi$ , then the union $T_1\cup T_2$ is consistent.

References

Boolos, George S.; Burgess, John P.; Jeffrey, Richard C. (2002). Computability and Logic. Cambridge University Press. pp. 264. ISBN 0521007585. http://books.google.com/books?id=Yy14JSjPyY8C.

‹The stub template below has been proposed for renaming to . See stub types for deletion to help reach a consensus on what to do.
Feel free to edit the template, but the template must not be blanked, and this notice must not be removed, until the discussion is closed. For more information, read the guide to deletion.›